typedef void ** __builtin_va_list;
typedef void ** __builtin_ms_va_list;

void __builtin_va_start(void *ap, ...);
void __builtin_va_end(void *ap);
void __builtin_va_copy(__builtin_va_list dest, __builtin_va_list src);
void __builtin_ms_va_start(void *ap, ...);
void __builtin_ms_va_end(void *ap);
void *__builtin_va_arg_pack();
int __builtin_va_arg_pack_len();
int __builtin_constant_p();
int __builtin_abs(int);
int __builtin_finite(double);
int __builtin_finitef(float);
int __builtin_finitel(long double);
int __builtin_fpclassify(int, int, int, int, int, ...);
int __builtin_isfinite();
int __builtin_isinf_sign();
int __builtin_isnanl(long double);
int __builtin_isnormal();
int __builtin_isgreater();
int __builtin_isgreaterequal();
int __builtin_isless();
int __builtin_islessequal();
int __builtin_islessgreater();
int __builtin_isunordered();
long int __builtin_labs(long);
long long int __builtin_llabs(long long int);
double __builtin_cos(double);
float __builtin_cosf(float);
double __builtin_fabs(double);
float __builtin_fabsf(float);
int __builtin_memcmp(const void *s1, const void *s2, __CPROVER_size_t n);
void *__builtin_memcpy(void *dest, const void *src, __CPROVER_size_t n);
void *__builtin___memcpy_chk(void *dest, const void *src, __CPROVER_size_t n, __CPROVER_size_t size);
char *__builtin___memmove_chk(void *dest, const void *src, __CPROVER_size_t n, __CPROVER_size_t size);
double __builtin_sin(double);
float __builtin_sinf(float);
double __builtin_sqrt(double);
float __builtin_sqrtf(float);
int __builtin_strcmp(const char *s1, const char *s2);
__CPROVER_size_t __builtin_strlen(const char *s);
int __builtin_strncmp(const char *s1, const char *s2, __CPROVER_size_t n);
void __builtin_abort();
void __builtin_prefetch(void *, ...);
int __builtin_printf(const char *fmt, ...);
int __builtin_fprintf(void *stream, const char *fmt, ...);
int __builtin_fscanf(void *stream, const char *fmt, ...);
int __builtin_scanf(const char *str, const char *fmt, ...);
int __builtin_fputs(const char *s, void *stream);
int __builtin_vsnprintf(char * restrict str, __CPROVER_size_t size, const char * restrict format, __builtin_va_list ap);
long __builtin_expect(long, long);
void *__builtin_memset(void *s, int c, __CPROVER_size_t n);
void *__builtin___memset_chk(void *s, int c, __CPROVER_size_t n, __CPROVER_size_t size);
void *__builtin_memchr(const void *s, int c, __CPROVER_size_t n);
void *__builtin_memmove(void *s1, const void *s2, __CPROVER_size_t n);
void *__builtin_mempcpy(void *, const void *, __CPROVER_size_t);
void *__builtin___mempcpy_chk(void *dest, const void *src,  __CPROVER_size_t n, __CPROVER_size_t size);
char *__builtin_strcat(char *dest, const char *src);
char *__builtin___strcat_chk(char *dest, const char *src, __CPROVER_size_t size);
char *__builtin_strcpy(char *dest, const char *src);
char *__builtin___strcpy_chk(char *dest, const char *src, __CPROVER_size_t size);
char *__builtin_strncpy(char *dest, const char *src, __CPROVER_size_t n);
char *__builtin___strncpy_chk(char *dest, const char *src, __CPROVER_size_t n, __CPROVER_size_t size);
char *__builtin_stpcpy(char *dest, const char *src);
char *__builtin___stpcpy(char *s1, const char *s2);
char *__builtin___stpncpy_chk(char *s1, const char *s2, __CPROVER_size_t n, __CPROVER_size_t size);
int __builtin___sprintf_chk(char *s, int flag, __CPROVER_size_t os, const char *fmt, ...);
int __builtin___snprintf_chk(char *s, __CPROVER_size_t maxlen, int flag, __CPROVER_size_t os, const char *fmt, ...);
int __builtin___vsprintf_chk(char *s, int flag, __CPROVER_size_t os, const char *fmt, __builtin_va_list ap);
int __builtin___vsnprintf_chk (char *s, __CPROVER_size_t maxlen, int flag, __CPROVER_size_t os, const char *fmt, __builtin_va_list ap);
void __builtin_exit(int status);
char *__builtin_strchr(const char *s, int c);
__CPROVER_size_t __builtin_strspn(const char *s, const char *accept);
__CPROVER_size_t __builtin_strcspn(const char *s, const char *reject);
char *__builtin_strstr(const char *a, const char *b);
char *__builtin_strpbrk(const char *s, const char *accept);
char *__builtin_strrchr(const char *s, int c);
char *__builtin_strncat(char *dest, const char *src, __CPROVER_size_t n);
char *__builtin___strncat_chk(char *dest, const char *src, __CPROVER_size_t n, __CPROVER_size_t size);
char *__builtin___stpcpy_chk(char *dest, const char *src, __CPROVER_size_t size);
void *__builtin_alloca(__CPROVER_size_t s);
int __builtin_ffs(int i);
char *__builtin_index(const char *s, int c);
char *__builtin_rindex(const char *s, int c);
int __builtin_bcmp(const void *s1, const void *s2, __CPROVER_size_t n);
void __builtin_bzero(void *s, __CPROVER_size_t n);
long double __builtin_sinl(long double x);
long double __builtin_cosl(long double x);
long double __builtin_sqrtl(long double x);
long double __builtin_fabsl(long double x);
int __builtin_popcount(unsigned int x);
int __builtin_popcountll(unsigned long long int x);
float __builtin_huge_valf();
double __builtin_huge_val();
float __builtin_inff();
double __builtin_inf();
float __builtin_nanf(const char *);
double __builtin_nan(const char *);
float __builtin_nansf(const char *);
double __builtin_nans(const char *);
long double __builtin_infl();
__CPROVER_size_t __builtin_object_size();
void *__builtin_return_address(unsigned level);
void *__builtin_extract_return_addr(void *);
int __builtin_choose_expr(_Bool, ...);
int __sync_fetch_and_add();
int __sync_fetch_and_sub();
int __sync_fetch_and_or();
int __sync_fetch_and_and();
int __sync_fetch_and_xor();
int __sync_fetch_and_nand();
int __sync_add_and_fetch();
int __sync_sub_and_fetch();
int __sync_or_and_fetch();
int __sync_and_and_fetch();
int __sync_xor_and_fetch();
int __sync_nand_and_fetch();
_Bool __sync_bool_compare_and_swap();
int __sync_val_compare_and_swap();
void __sync_synchronize();
int __sync_lock_test_and_set();
void __sync_lock_release();
float __builtin_acosf(float);
long double __builtin_acosl(long double);
float __builtin_asinf(float);
long double __builtin_asinl(long double);
float __builtin_atanf(float);
long double __builtin_atanl(long double);
float __builtin_atan2f(float, float);
long double __builtin_atan2l(long double, long double);
float __builtin_ceilf(float);
long double __builtin_ceill(long double);
float __builtin_coshf(float);
long double __builtin_coshl(long double);
float __builtin_expf(float);
long double __builtin_expl(long double);
float __builtin_floorf(float);
long double __builtin_floorl(long double);
float __builtin_fmodf(float, float);
long double __builtin_fmodl(long double, long double);
float __builtin_frexpf(float, int*);
long double __builtin_frexpl(long double, int*);
float __builtin_ldexpf(float , int exp);
long double __builtin_ldexpl(long double, int);
float __builtin_logf(float);
long double __builtin_logl(long double);
float __builtin_log10f(float);
double __builtin_log10(double);
long double __builtin_log10l(long double);
float __builtin_log2f(float);
double __builtin_log2(double);
long double __builtin_log2l(float);
float __builtin_modff(float, float*);
long double __builtin_modfl(long double, long double*);
float __builtin_powf(float, float);
long double __builtin_powl(long double, long double);
double __builtin_powi(double, int);
float __builtin_powif(float, int);
long double __builtin_powil(long double, int);
float __builtin_sinhf(float);
long double __builtin_sinhl(long double);
float __builtin_tanf(float);
long double __builtin_tanl(long double);
float __builtin_tanhf(float);
long double __builtin_tanhl(long double);
int __builtin_parityl(unsigned long);
int __builtin_parityll(unsigned long long);
void __builtin_trap(void);
void __builtin___clear_cache(char *begin, char *end);
int __builtin_clz(unsigned int);
int __builtin_clzll(unsigned long long);
int __builtin_ctz(unsigned int);
int __builtin_ctzll(unsigned long long);
int __builtin_parity(unsigned int);
int __builtin_ffsl(unsigned long);
int __builtin_clzl(unsigned long);
int __builtin_ctzl(unsigned long);
short unsigned int __builtin_bswap16(short unsigned int);
long unsigned int __builtin_bswap32(long unsigned int);
long long unsigned int __builtin_bswap64(long long unsigned int);
int __builtin_classify_type();
int __builtin_isinf(double);
int __builtin_isinff(float);
int __builtin_isinfl(long double);
int __builtin_isnan(double);
int __builtin_isnanf(float);
int __builtin_signbit(double);
int __builtin_signbitf(float);
int __builtin_signbitl(long double);

void __builtin_unreachable(void);

typedef int    __gcc_m64   __attribute__ ((__vector_size__ (8), __may_alias__));

typedef char   __gcc_v8qi  __attribute__ ((__vector_size__ (8)));
typedef char   __gcc_v16qi __attribute__ ((__vector_size__ (16)));
typedef char   __gcc_v32qi __attribute__ ((__vector_size__ (32)));
typedef int    __gcc_v2si  __attribute__ ((__vector_size__ (8)));
typedef int    __gcc_v4si  __attribute__ ((__vector_size__ (16)));
typedef int    __gcc_v8si  __attribute__ ((__vector_size__ (32)));
typedef int    __gcc_v16si  __attribute__ ((__vector_size__ (64)));
typedef short  __gcc_v4hi  __attribute__ ((__vector_size__ (8)));
typedef short  __gcc_v8hi  __attribute__ ((__vector_size__ (16)));
typedef short  __gcc_v16hi __attribute__ ((__vector_size__ (32)));
typedef short  __gcc_v32hi __attribute__ ((__vector_size__ (64)));
typedef float  __gcc_v2sf  __attribute__ ((__vector_size__ (8)));
typedef float  __gcc_v4sf  __attribute__ ((__vector_size__ (16)));
typedef float  __gcc_v8sf  __attribute__ ((__vector_size__ (32)));
typedef float  __gcc_v16sf  __attribute__ ((__vector_size__ (64)));
typedef double __gcc_v2df  __attribute__ ((__vector_size__ (16)));
typedef double __gcc_v4df  __attribute__ ((__vector_size__ (32)));
typedef double __gcc_v8df  __attribute__ ((__vector_size__ (64)));
typedef long long __gcc_v1di __attribute__ ((__vector_size__ (8)));
typedef long long __gcc_v2di __attribute__ ((__vector_size__ (16)));
typedef long long __gcc_v4di __attribute__ ((__vector_size__ (32)));
typedef long long __gcc_v8di __attribute__ ((__vector_size__ (64)));
typedef unsigned long long __gcc_di;

enum __gcc_atomic_memmodels {
  __ATOMIC_RELAXED, __ATOMIC_CONSUME, __ATOMIC_ACQUIRE, __ATOMIC_RELEASE, __ATOMIC_ACQ_REL, __ATOMIC_SEQ_CST
};
